TerminationOnIrrelevant.agda:14,4-7
Cannot pattern match against irrelevant argument of type Empty
when checking that the pattern c x has type Empty
